Step of Proof: branch-ifthenelse 11,40

Inference at * 1 1 
Iof proof for Lemma branch-ifthenelse:



1. b : 
2. P : Top
3. Q : Top
4. x : b
5. bool-decider(b) = (inl x )
  P ~ if b then P else Q fi  
latex

 by AutoBoolCase b 
latex


 .


Definitionsleft + right, Unit, P  Q, P & Q, x:A  B(x), x:AB(x), , s = t, b, b, x:AB(x), t  T, , A, P  Q, False
Lemmaseqtt to assert, iff transitivity, eqff to assert, assert of bnot, assert wf, bnot wf, not wf, bool wf

origin